∂03-OCT-74  1737		FOO,DBA
 SOFT.TK[FOO,DBA] is Tom Knight's opinion.

∂03-OCT-74  0015		VCG,DCL
 I THINK OCT 12-13 WILL BE GOOD.
 MAJA RETURNS OCT 8; I'LL ASK HER THEN.
 WE SHOULD START ON THE PROPSAL; THE GENERAL IDEA
 IS A PROGRAMMING LABORATORY,ONE COMPONENT BEING
 A VERIFYING COMPILER FOR PASCAL.MAYBE FOR LISP TOO.
 METHOD.PUB  AND METH3.PUB WILL FILL WHATS GONE ON
 WITH THE VERIFIER RECENTLY--DAVID
 PS HOWS THE APG SYSTEM?

∂01-OCT-74  1520		VCG,DCL
 1. THE LATEST PUMP FILES SEEM TO BE:
 FPUMP1.TST AND FPUMP.TST.
 THESE DO NOT HAVE ITERATIVE RULES, BUT OF COURSE
 THEY SHOULD WORK!
 YOU CAN TRY CLEANING UP JACKS TRANSLATION FRAME:
 FTSL, WHICH HAS CONDITIONALS INSIDE LOOPS AND 
 IS A REAL TEST.
 I NOTICE ALSO A FRAME CALLED "FBADIT.PMP" WHICH WAS
 INTENDED TO BE AN ITERATION RULE FOR THE PUMPING
 FRAMES.
 2. IF YOU DON'T NEED *.JRA ON[APG,DCL] ANYMORE,PLEASE
 ERASE.
 3.I'VE FINISHED THE VERIFICATION PAPER(ROUGH DRAFT)
 IS ON"METHOD.PUB" AND "METH3.PUB" [VCG,DCL].
 COMMENTS WOULD BE APPRECIATED.
 4. WE MUST START NOW ON THE PROPOSAL-DAVID
∂30-SEP-74  1442		1,MG
 I've just noticed that the definition of fact in problem IV on p71.
 of "SUPER LISP"is an application of the Y combinator (λf.((λx.f(xx))(λx.f(xx))))
 If you wanted to discuss Y pehaps that example would be a good place to start?

∂30-SEP-74  0929		1,MG
 Unfortunately I don't know anything non-trivial about modelling data-structures
 The only thing that comes to mind is Rod Burstall's stuff in MI7 (I think !)
 which is about how to represent & reason about pointer manipulating
 algorithms.Although that's a good paper the data-structure models in it
 arn't all that subtle - the nice thing in the paper is an efficient
 formalism (informally presented if I remember right) for asserting facts
 about pointer configurations. I hope to extend my denotational model of LISP
 to include RPLACA,RPLACD etc. but, probably naively, I hadn't thought that
 doing it would raise any hard problems. I guess time will tell!
                           Mike